T:Type, as, bs:(T List). no_repeats(T;as @ bs)  no_repeats(T;bs @ as) 

latex

Definitions	as @ bs, no_repeats(T;l), P  Q, type List, x:A. B(x), Type, t  T, s = t, A, a < b, A  B, , ||as||, Void, x:AB(x), False, {x:A| B(x)} , , #$n, l[i], , |g|, S  T, left + right, P  Q, Dec(P), b, x:A  B(x), x:A. B(x), b | a, a ~ b, a  b, a <p b, a < b, A c B, f(a), x f y, xL. P(x), (xL.P(x)), n+m, P  Q, P & Q, P  Q, n - m, True, T, {i..j}, i  j < k, i  j , -n, (x  l)
Lemmas	no repeats wf, select append front, member wf, non neg length, select append back, true wf, le wf, squash wf, iff wf, rev implies wf, length append, decidable lt, length wf1, append wf, nat wf, not wf, select wf